Nuprl Lemma : es-E-interface-image
11,40
postcript
pdf
es
:ES,
A
,
B
:Type,
f
:(
A
B
),
Ia
:AbsInterface(
A
). (E(
f
'
Ia
)
r E(
Ia
)) & (E(
Ia
)
r E(
f
'
Ia
))
latex
Definitions
x
:
A
.
B
(
x
)
,
AbsInterface(
A
)
,
P
&
Q
,
Top
,
P
Q
,
t
T
,
S
T
,
suptype(
S
;
T
)
,
Lemmas
es-E-interface
functionality
,
es-interface-image
wf
,
top
wf
,
subtype
rel
function
,
es-E
wf
,
subtype
rel
sum
,
assert
wf
,
es-is-interface
wf
,
es-interface
wf
,
event
system
wf
,
es-is-interface-image
origin
es:ES, A, B:Type, f:(A
B), Ia:AbsInterface(A). (E(f'Ia) 
r E(Ia)) & (E(Ia) r E(f'Ia)) es:ES, A, B:Type, f:(AB), Ia:AbsInterface(A). (E(f'Ia) r E(Ia)) & (E(Ia) r E(f'Ia)) 
Q
T